b:. (0  b2i(b)) & (b2i(b)  1) 

latex

ProofTree

Definitions	t  T, x:A. B(x), ff, False, P  Q, A, if b then t else f fi , tt, b2i(b), A  B, P & Q, Unit, ,
Lemmas	bool wf